(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
head(Cons(x, xs)) → x
e(Cons(F, Nil), b) → False
e(Cons(T, Nil), b) → False
e(Cons(B, Nil), b) → False
e(Cons(A, Nil), b) → e[Match][Cons][Ite][True][Match](A, Nil, b)
e(Cons(F, Cons(x, xs)), b) → False
e(Cons(T, Cons(x, xs)), b) → False
e(Cons(B, Cons(x, xs)), b) → False
e(Cons(A, Cons(x, xs)), b) → False
equal(F, F) → True
equal(F, T) → False
equal(F, B) → False
equal(F, A) → False
equal(T, F) → False
equal(T, T) → True
equal(T, B) → False
equal(T, A) → False
equal(B, F) → False
equal(B, T) → False
equal(B, B) → True
equal(B, A) → False
equal(A, F) → False
equal(A, T) → False
equal(A, B) → False
equal(A, A) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
e(Nil, b) → False
t(x, y) → t[Ite](e(x, y), x, y)
r(x, y) → r[Ite](e(x, y), x, y)
q(x, y) → q[Ite](e(x, y), x, y)
p(x, y) → p[Ite](e(x, y), x, y)
goal(x, y) → q(x, y)
The (relative) TRS S consists of the following rules:
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
q[Ite](False, x', Cons(F, Cons(F, xs))) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))
q[Ite](False, x, Cons(F, Cons(T, xs))) → False
q[Ite](False, x, Cons(F, Cons(B, xs))) → False
q[Ite](False, x, Cons(F, Cons(A, xs))) → False
q[Ite](False, x, Cons(T, Cons(F, xs))) → False
q[Ite](False, x, Cons(T, Cons(T, xs))) → False
q[Ite](False, x, Cons(T, Cons(B, xs))) → False
q[Ite](False, x, Cons(T, Cons(A, xs))) → False
q[Ite](False, x, Cons(B, Cons(F, xs))) → False
q[Ite](False, x, Cons(B, Cons(T, xs))) → False
q[Ite](False, x, Cons(B, Cons(B, xs))) → False
q[Ite](False, x, Cons(B, Cons(A, xs))) → False
q[Ite](False, x, Cons(A, Cons(F, xs))) → False
q[Ite](False, x, Cons(A, Cons(T, xs))) → False
q[Ite](False, x, Cons(A, Cons(B, xs))) → False
q[Ite](False, x, Cons(A, Cons(A, xs))) → False
q[Ite](False, x', Cons(F, Nil)) → q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))
q[Ite](False, x', Cons(T, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))
q[Ite](False, x', Cons(B, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))
q[Ite](False, x', Cons(A, Nil)) → q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))
r[Ite](False, x', Cons(F, xs)) → r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))
r[Ite](False, x, Cons(T, xs)) → False
r[Ite](False, x, Cons(B, xs)) → False
r[Ite](False, x, Cons(A, xs)) → False
p[Ite](False, x', Cons(F, xs)) → and(r(x', Cons(F, xs)), p(x', xs))
p[Ite](False, x, Cons(T, xs)) → False
p[Ite](False, x, Cons(B, xs)) → False
p[Ite](False, x, Cons(A, xs)) → False
q[Ite][False][Ite](True, x', Cons(x, xs)) → q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))
t[Ite](False, x, y) → True
t[Ite](True, x, y) → True
r[Ite](True, x, y) → True
q[Ite](True, x, y) → True
q[Ite][False][Ite](False, x, y) → False
p[Ite](True, x, y) → True
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
r(Cons(F, Nil), Cons(F, xs8693_0)) →+ r[Ite][False][Ite][True][Ite](and(q(Cons(F, Nil), xs8693_0), r(Cons(F, Nil), xs8693_0)), Cons(F, Nil), Cons(F, xs8693_0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1].
The pumping substitution is [xs8693_0 / Cons(F, xs8693_0)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)